﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Goals;

namespace MicroBenchmarks.SumInCondition
{
    /// <summary>
    /// Checks the scenario where fields from multiple classes are involved
    /// in a conditional check 
    /// </summary>
    [PexClass]
    [PexMe.Attribute.FieldAccessObserver]
    [PexMe.Attribute.InsufficientObjectFactoryObserver]
    public partial class SummationTest
    {
        [PexMethod]
        [PexAssertReachEventually]
        public void TestSummationPUT([PexAssumeUnderTest]FieldClass1 fc1, [PexAssumeUnderTest]FieldClass2 fc2)
        {
            if (fc1.Field1 + fc2.Field2 > 5)
                PexAssert.ReachEventually();
        }
    }
}
